(VAR X Y)
(STRATEGY CONTEXTSENSITIVE 
  (from 1)
  (cons 1)
  (s 1)
  (length)
  (nil)
  (0)
  (length1)
)
(RULES 
from(X) -> cons(X,from(s(X)))
length(nil) -> 0
length(cons(X,Y)) -> s(length1(Y))
length1(X) -> length(X)
)